/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */

package tracetoautomata;

import alloytoy.Util;
import java.io.BufferedWriter;
import java.io.FileWriter;
import java.io.IOException;
import java.io.PrintWriter;
import java.util.*;

/**
 * A DFA representation.
 * @author daniel
 */
public class DFA {

    public Map<State,ArrayList<State>> graph;
    public ArrayList<State> nStates;
    public ArrayList<State> finals;


    public DFA(){
        graph = new HashMap<State,ArrayList<State>>();
        nStates = new ArrayList<State>();
        finals = new ArrayList<State>();
    }

    public DFA(ArrayList<State> states){
        graph = new HashMap<State,ArrayList<State>>();
        nStates = new ArrayList<State>();
        finals = new ArrayList<State>();

        for(int i=0; i<states.size(); i++){
            ArrayList<State> tmp = new ArrayList<State>();
            if(i<states.size()-1){
                tmp.add(states.get(i+1));
            }
            graph.put(states.get(i), tmp);
            nStates.add(states.get(i));
        }
        if(states.size()>0)
            finals.add(states.get(states.size()-1));
    }

    public int findIndexEquals(ArrayList<State> list, State state)
    {
        for(int i=0; i<list.size(); i++)
        {
            if(list.get(i).MyEquals(state)) return i;
        }
        return -1;
    }
    //First states are equal.
    public void UniteDFA(DFA other)
    {
        if(this.nStates.isEmpty()){
            this.nStates = other.nStates;
            this.finals = other.finals;
            this.graph = other.graph;
        }

        if(other.nStates.size()>0 && this.nStates.size()>0)
        {
            //First states are equal.
            int pos = findIndexEquals(this.nStates,other.nStates.get(0));
            if(pos!=-1)
                this.addNodes(this.nStates.get(pos),other.graph.get(other.nStates.get(0)),other);
            else
                this.addNodes(this.nStates.get(0),other.graph.get(other.nStates.get(0)),other);
            for(int i=1; i<other.nStates.size(); i++)
            {
                this.addNodes(other.nStates.get(i), other.graph.get(other.nStates.get(i)), other);
            }
        }
    }

    public void addNodes(State from, ArrayList<State> states, DFA other)
    {
        if(!states.isEmpty())
        {
            for(State s : states)
            {
                this.addNode(from, s);
                if(other.finals.contains(s))
                    this.finals.add(s);
            }
        }
        else{
            this.addNode(from);
        }
    }

    public void addNode(State from)
    {
        if(!nStates.contains(from)) nStates.add(from);
        ArrayList<State> nodes = graph.get(from);
        if(nodes==null)
        {
            nodes = new ArrayList<State>();
            graph.put(from, nodes);
        }
    }

    public void addNode(State from, State to){
        ArrayList<State> nodes = graph.get(from);
        if(nodes!=null){
            if(!nStates.contains(to)) nStates.add(to);

            nodes.add(to);
        }
        else{
            nodes = new ArrayList<State>();
            if(!nStates.contains(from)) nStates.add(from);
            if(!nStates.contains(to)) nStates.add(to);
            nodes.add(to);
        }

        graph.put(from,nodes);
    }
    
    public void PrintViz(String fileName)
    {
        try{
            // Create file
            PrintWriter pw = new PrintWriter(new FileWriter(fileName));
            pw.write("digraph G {\n");
            HashMap<String, ArrayList<String>> stateDescription = new HashMap<String, ArrayList<String>>();
            
            for(int i=0; i<nStates.size(); i++)
            {
                ArrayList<String> descriptions = stateDescription.get(nStates.get(i).getDescription());
                if(descriptions==null)
                    descriptions = new ArrayList<String>();
                
                //String tmp ="[";
                for(State st : graph.get(nStates.get(i)))
                {
                    if(!descriptions.contains(st.getDescription()))
                    {
                        descriptions.add(st.getDescription());
                        //String s = nStates.get(i).getDescription()+i + "->" + st.getDescription()+nStates.indexOf(st)+";\n";

                        String s = nStates.get(i).getDescription()+ "->" + st.getDescription()+";\n";
                        //String s = "\""+Integer.toString(i) + "\"->" + "\""+this.nStates.indexOf(st)+"\"\n";
                        //stateDescription.put("\""+Integer.toString(i),nStates.get(i).getDescription());
                        //stateDescription.put("\""+this.nStates.indexOf(st),st.getDescription());
                        pw.write(s);
                    }
                }

                stateDescription.put(nStates.get(i).getDescription(),descriptions);
                //tmp+="]";
                //System.out.println(i + "->"+ tmp);
            }

            pw.write("}");
            pw.flush();
            //Close the output stream
            //WriteDescription(fileName, stateDescription);
            //System.out.println(fileName);
            //System.out.println(stateDescription);

        }catch (Exception e){//Catch exception if any
          System.err.println("Error: " + e.getMessage());
        }
    }

    public void WriteDescription(String fileName, HashMap<String,String> descriptions) throws IOException
    {
        PrintWriter pw = new PrintWriter(new FileWriter(fileName+".desc"));

        for(String s : descriptions.keySet())
        {
            pw.write(s+"\n");
            pw.write(descriptions.get(s));
            pw.write("\n\n");
        }
        pw.flush();
        pw.close();
    }

    public void PrintAutomaton(){

        for(int i=0; i<nStates.size(); i++)
        {
            String tmp ="[";
            for(State st : graph.get(nStates.get(i)))
            {
                tmp+=Integer.toString(nStates.indexOf(st))+" "+st.getAllRels()+",";
            }
            tmp+="]";
            System.out.println(i + "->"+ tmp);
        }

        System.out.print("Finals: ");
        for(State s :this.finals)
        {
            System.out.print("["+this.nStates.indexOf(s)+"]");
        }
        System.out.println("");
    }



    public void MinimizeDFA()
    {
        //1. Set up a table of all pairs of states {q, q'} with q  q' of M.
        boolean[][] marks = new boolean[this.nStates.size()][this.nStates.size()];
        //2. Mark all pairs {q, q'} with q  F and q'  F (or vice versa).
        for(int i=0; i<this.nStates.size(); i++)
        {
            for(int j=0; j<this.nStates.size(); j++)
            {
                if(j!=i)
                {
                    if(finals.contains(nStates.get(i)) && !finals.contains(nStates.get(j)))
                    {
                        marks[i][j]=true;
                        marks[j][i]=true;
                    }
                    if(!finals.contains(nStates.get(i)) && finals.contains(nStates.get(j)))
                    {
                        marks[i][j]=true;
                        marks[j][i]=true;
                    }
                }
            }
        }

        //3. For each unmarked pair {q, q'} and each a , test, if {(q,a), (q',a)} is already marked. If so: mark {q, q'} as well.
        //4. Repeat the last step until it produces no changes in the table any more.
        boolean changes=true;
        while(changes)
        {
            changes=false;
            for(int i=0; i<this.nStates.size(); i++)
            {
                for(int j=0; j<this.nStates.size(); j++)
                {
                    if(j!=i && !marks[i][j])
                    {
                        if(!nStates.get(i).MyEquals(nStates.get(j)))
                        {
                           marks[i][j]=true;
                           marks[j][i]=true;
                           changes=true;
                        }
                    }
                }
            }
        }

        /*for(int i=0; i<this.nStates.size(); i++)
        {
            System.out.println("");
            for(int j=0; j<this.nStates.size(); j++)
            {
                System.out.print(i+""+marks[i][j]+""+j+" ");

            }
        }*/


        //Unite all unmarked pairs of states {q, q'} after the following rules:
        //(1) if (p, a, q')   with p Q, a  then:   =   (p, a, q)
        //(2) if (q', a, p)   with p Q, a  then:   =   (q, a, p)
        //(3) remove q' from Q
        //(4) remove (p, a, q') and (q', a, p) from  for all p Q, a
        ArrayList<Integer> removes = new ArrayList<Integer>();
        for(int i=0; i<this.nStates.size(); i++)
        {
            for(int j=0; j<this.nStates.size(); j++)
            {
                if(!marks[i][j] && i!=j)
                {
                    for(State p : nStates)
                    {
                        //(1)
                        if(graph.get(p).contains(nStates.get(j))){
                            if(!graph.get(p).contains(nStates.get(i)))
                                addNode(p,nStates.get(i));
                        }
                        //(2)
                        if(graph.get(nStates.get(j)).contains(p)){
                            if(!graph.get(nStates.get(i)).contains(p))
                                addNode(nStates.get(i),p);
                        }

                        //(4)
                        ArrayList<State> pStates = graph.get(p);

                        pStates.remove(nStates.get(j));
                        ArrayList<State> iStates = graph.get(nStates.get(j));
                        iStates.remove(p);
                        graph.put(p,pStates);
                        graph.put(nStates.get(j),iStates);

                    }
                    //(3)
                    //removes.add(j);
                    //nStates.remove(j);
                }
            }
        }

        boolean change=true;
        int i=-1;
        while(change)
        {
            change=false;
            for(State s : nStates)
            {
                if(!finals.contains(s) && graph.get(s).isEmpty())
                {
                    i = nStates.indexOf(s);
                    change=true;
                }
            }
            if(change)
                nStates.remove(i);
        }
    }
}